<html>
<head><meta charset="utf-8"><title>AliasEq question · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html">AliasEq question</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="200040741"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200040741" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200040741">(Jun 07 2020 at 20:27)</a>:</h4>
<p>Does <code>AliasEq(&lt;T as Trait&gt;::*, *)</code> implicitly assume that someone proved <code>Implemeted(T: Trait)</code>? I am a little surprised that</p>
<div class="codehilite"><pre><span></span><code>forall&lt;T&gt; {
    exists&lt;U&gt; {
        AliasEq(&lt;T as Iterator&gt;::Item, U)
   }
}
</code></pre></div>


<p>is provable. (Mind you, <code>AliasEq</code> is not a real goal in <code>.chalk</code> syntax at the moment,  I added it for debug purposes)</p>



<a name="200042695"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200042695" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200042695">(Jun 07 2020 at 21:15)</a>:</h4>
<p>Wouldn't WF checks handle that?</p>



<a name="200042763"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200042763" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200042763">(Jun 07 2020 at 21:16)</a>:</h4>
<p>I mean, that <code>T as Trait</code> has to come from some item, and that item should be well-formed</p>



<a name="200046591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200046591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200046591">(Jun 07 2020 at 22:52)</a>:</h4>
<p><span class="user-mention" data-user-id="251766">@Areredify</span> you probably are looking for <code>Normalize</code></p>



<a name="200046598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200046598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200046598">(Jun 07 2020 at 22:52)</a>:</h4>
<p>But yes, the <code>T as Iterator</code> part is only okay because of WF checks</p>



<a name="200046667"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200046667" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200046667">(Jun 07 2020 at 22:54)</a>:</h4>
<p>So, like, in the parser, we would lower <code>T: Iterator&lt;Item=U&gt;</code> as two where clauses: <code>T: Iterator</code> and <code>ProjectionEq(&lt;T as Iterator&gt;::Item = U)</code></p>



<a name="200061437"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200061437" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200061437">(Jun 08 2020 at 06:13)</a>:</h4>
<p>I know that</p>



<a name="200061447"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200061447" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200061447">(Jun 08 2020 at 06:13)</a>:</h4>
<p>This example was generated by chalk in wf checks</p>



<a name="200062354"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200062354" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200062354">(Jun 08 2020 at 06:34)</a>:</h4>
<p>In this example (<code>assoc_tys</code>)</p>
<div class="codehilite"><pre><span></span><code>struct String { }
struct Char { }

trait Iterator { type Item; }
impl Iterator for String { type Item = Char; }

trait Foo { }
impl&lt;X&gt; Foo for &lt;X as Iterator&gt;::Item where X: Iterator { }
</code></pre></div>


<p>wf checks for <code>Foo</code> generate a goal</p>
<div class="codehilite"><pre><span></span><code>forall&lt;T&gt; {
    LocalImplAllowed(&lt;T as Iterator&gt;::Item: Foo)
}
</code></pre></div>



<a name="200062377"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200062377" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200062377">(Jun 08 2020 at 06:35)</a>:</h4>
<p>which is provable but technically T doesn't implement iterator</p>



<a name="200067942"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200067942" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200067942">(Jun 08 2020 at 08:09)</a>:</h4>
<p>So...that's not a valid program...</p>



<a name="200068008"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200068008" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200068008">(Jun 08 2020 at 08:10)</a>:</h4>
<p><a href="https://play.rust-lang.org/?version=stable&amp;mode=debug&amp;edition=2018&amp;gist=f10f6686f3d66b800a9ccca35f1701c4">https://play.rust-lang.org/?version=stable&amp;mode=debug&amp;edition=2018&amp;gist=f10f6686f3d66b800a9ccca35f1701c4</a></p>



<a name="200068044"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200068044" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200068044">(Jun 08 2020 at 08:10)</a>:</h4>
<p>That test is wrong I think</p>



<a name="200074114"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200074114" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200074114">(Jun 08 2020 at 09:19)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> is it invalid or just a limitation of the rustc trait system?</p>



<a name="200074724"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200074724" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Matthew Jasper <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200074724">(Jun 08 2020 at 09:26)</a>:</h4>
<p>It's actually invalid. Allowing it would result in overlapping implementations of <code>Foo</code> for a type. For example <code>&amp;i32</code> would be implemented for both <code>X = std::option::Iter&lt;'_, i32&gt;</code> and <code>X = std::slice::Iter&lt;'_, i32&gt;</code></p>



<a name="200075106"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200075106" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200075106">(Jun 08 2020 at 09:31)</a>:</h4>
<p>...oh</p>



<a name="200075298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200075298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200075298">(Jun 08 2020 at 09:33)</a>:</h4>
<p>Coherence rules regarding associated items are in a little bit of a mess right now, iirc</p>
<div class="codehilite"><pre><span></span><code> impl&lt;I&gt; Foo for I where I: Iterator&lt;Item = u8&gt; {}
 impl&lt;I&gt; Foo for I where I: Iterator&lt;Item = u8&gt; {}
</code></pre></div>


<p>is still allowed in chalk</p>



<a name="200075329"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200075329" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200075329">(Jun 08 2020 at 09:34)</a>:</h4>
<p>Anyway, doesn't really change my question</p>



<a name="200075403"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200075403" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200075403">(Jun 08 2020 at 09:34)</a>:</h4>
<p>That is, is this inteded to be provable or not? </p>
<div class="codehilite"><pre><span></span><code>forall&lt;T&gt; {
    exists&lt;U&gt; {
        AliasEq(&lt;T as Iterator&gt;::Item, U)
   }
}
</code></pre></div>



<a name="200076769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200076769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200076769">(Jun 08 2020 at 09:51)</a>:</h4>
<p>Seems like it's the same question as well-formedness of tuples and arrays</p>



<a name="200077031"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200077031" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Areredify <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200077031">(Jun 08 2020 at 09:54)</a>:</h4>
<p>The difference is that chalk produced the ill-formed type (&lt;T as Iterator&gt;::Item) instead of it being passed from outside</p>



<a name="200160652"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200160652" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200160652">(Jun 08 2020 at 21:53)</a>:</h4>
<p>I'm not sure what I think the answer should be</p>



<a name="200160688"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200160688" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200160688">(Jun 08 2020 at 21:53)</a>:</h4>
<p>it seems clear that somebody needs to prove that <code>T: Iterator</code></p>



<a name="200160706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200160706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200160706">(Jun 08 2020 at 21:53)</a>:</h4>
<p>but should it be that <code>AliasEq</code> rules, or a seperate WF check, is I guess the question</p>



<a name="200160756"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200160756" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200160756">(Jun 08 2020 at 21:54)</a>:</h4>
<p>in particular, I guess the question is whether the "placeholder rule" needs to require that <code>T: Iterator</code></p>



<a name="200160776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200160776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200160776">(Jun 08 2020 at 21:54)</a>:</h4>
<p>I don't remember if we elided it on purpose, <span class="user-mention" data-user-id="131694">@scalexm</span> might. Off the top of my head, I can't think of a good reason to do so.</p>



<a name="200237711"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200237711" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200237711">(Jun 09 2020 at 14:38)</a>:</h4>
<p>I agree, probably we elided it just because it was not strictly needed as <code>AliasEq</code> rules are never used directly, but rather are desugared from <code>T: Iterator&lt;Item = U&gt;</code></p>



<a name="200238324"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/AliasEq%20question/near/200238324" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> scalexm <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/AliasEq.20question.html#200238324">(Jun 09 2020 at 14:42)</a>:</h4>
<p>... or can come from unification during type checking, in which case we’ll also issue a <code>WF(&lt;T as Iterator&gt;::Item)</code>, which requires <code>Implemented(T: Iterator)</code> to be proved (I guess that’s what <span class="user-mention" data-user-id="116009">@nikomatsakis</span> was saying)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>